(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x7357185963068eab) #x0000000000000002))
(constraint (= (f #x1b72518134e2e867) #x0000000000000002))
(constraint (= (f #xe53d928e9249d340) #x94f64a3a49274d00))
(constraint (= (f #xa2d0e77859352029) #x8b439de164d480a4))
(constraint (= (f #x6bd9a67045786dac) #x6bd9a67045786dae))
(constraint (= (f #x3e4d34744ba01623) #x0000000000000002))
(constraint (= (f #x2304c3e0b9029e9a) #x2304c3e0b9029e9c))
(constraint (= (f #x2325e3442ab29b66) #x2325e3442ab29b68))
(constraint (= (f #xbe363e2e1e0e903d) #x0000000000000002))
(constraint (= (f #x93a296ee313e670b) #x0000000000000002))
(constraint (= (f #x2a4e8aad8856a823) #x0000000000000002))
(constraint (= (f #x27840ac0415c67ea) #x27840ac0415c67ec))
(constraint (= (f #x85ac5e7d89d3c575) #x16b179f6274f15d4))
(constraint (= (f #x2585e7101124705e) #x2585e71011247060))
(constraint (= (f #x0c6d9e3e2e083e09) #x0000000000000002))
(constraint (= (f #xe73488644e363be2) #xe73488644e363be4))
(constraint (= (f #x9b8ceee71894ee00) #x9b8ceee71894ee02))
(constraint (= (f #x65e22edbc552a183) #x0000000000000002))
(constraint (= (f #x7c48be800ec8ea82) #x7c48be800ec8ea84))
(constraint (= (f #x43d6d66e5d03793e) #x0f5b59b9740de4f8))
(constraint (= (f #x560703b8d86e9915) #x0000000000000002))
(constraint (= (f #x7e6b8d370234726a) #x7e6b8d370234726c))
(constraint (= (f #xb4e97a80d2b2b337) #x0000000000000002))
(constraint (= (f #xe1d72ce3c75255d7) #x0000000000000002))
(constraint (= (f #x7656db47edae0d67) #x0000000000000002))
(constraint (= (f #xe2b886c2eda835e0) #xe2b886c2eda835e2))
(constraint (= (f #x9eeeeebec0ab3466) #x7bbbbafb02acd198))
(constraint (= (f #x4aad4c90ec8dd1d0) #x2ab53243b2374740))
(constraint (= (f #x38bb9105aec0abc5) #x0000000000000002))
(constraint (= (f #x885a5a23a2485de2) #x885a5a23a2485de4))
(constraint (= (f #x38313e84d8312539) #xe0c4fa1360c494e4))
(constraint (= (f #x0544e2766db22528) #x0544e2766db2252a))
(constraint (= (f #x20a82c67cec4684e) #x20a82c67cec46850))
(constraint (= (f #x5c7754e1d07620de) #x5c7754e1d07620e0))
(constraint (= (f #xb8663ea8cea44735) #x0000000000000002))
(constraint (= (f #xedd9c4e81547e765) #xb76713a0551f9d94))
(constraint (= (f #x2e44356a4ead63ee) #xb910d5a93ab58fb8))
(constraint (= (f #x96e32ce6b85684e4) #x96e32ce6b85684e6))
(constraint (= (f #x55e1872400b57a15) #x57861c9002d5e854))
(constraint (= (f #x4a957127c2e72e29) #x2a55c49f0b9cb8a4))
(constraint (= (f #xd8d00e07e2cc351d) #x0000000000000002))
(constraint (= (f #xeb10939b0e50bb82) #xeb10939b0e50bb84))
(constraint (= (f #xb285bd5e7d536057) #xca16f579f54d815c))
(constraint (= (f #x3db10e7eab015c81) #xf6c439faac057204))
(constraint (= (f #x5321789a8cde3d57) #x0000000000000002))
(constraint (= (f #xaebb2e14257d1e3e) #xbaecb85095f478f8))
(constraint (= (f #x0cd435ab537bdd9e) #x3350d6ad4def7678))
(constraint (= (f #x27eeae3192eadeca) #x27eeae3192eadecc))
(constraint (= (f #x9d5d6deee8a0a700) #x9d5d6deee8a0a702))
(constraint (= (f #x8a1e283adb13e412) #x2878a0eb6c4f9048))
(constraint (= (f #x8eb2ce28c5a9225d) #x3acb38a316a48974))
(constraint (= (f #x10259aeed9a109e2) #x40966bbb66842788))
(constraint (= (f #x9cb9e8cc2781d635) #x72e7a3309e0758d4))
(constraint (= (f #x5868c9d75c66946c) #x5868c9d75c66946e))
(constraint (= (f #x5a89205182409ae2) #x5a89205182409ae4))
(constraint (= (f #xd7a845d933ad2d83) #x5ea11764ceb4b60c))
(constraint (= (f #x184deb6232a536e0) #x6137ad88ca94db80))
(constraint (= (f #x40030930d0571b09) #x000c24c3415c6c24))
(constraint (= (f #xbbaca57802b2d5cc) #xbbaca57802b2d5ce))
(constraint (= (f #xe1a4b380a51c191a) #xe1a4b380a51c191c))
(constraint (= (f #x04deb590a248131a) #x04deb590a248131c))
(constraint (= (f #x2c7277e7cc16e2d2) #x2c7277e7cc16e2d4))
(constraint (= (f #x4d2ae11d8e0bb6b7) #x34ab8476382edadc))
(constraint (= (f #xaecab9d9a163eceb) #xbb2ae766858fb3ac))
(constraint (= (f #x5e8883584e603c47) #x0000000000000002))
(constraint (= (f #xae0b9e896de3a032) #xb82e7a25b78e80c8))
(constraint (= (f #xb15897a0a9e2b759) #x0000000000000002))
(constraint (= (f #xc37ba6ab91bb01ce) #x0dee9aae46ec0738))
(constraint (= (f #xbb0c5ebe8890ed5e) #xbb0c5ebe8890ed60))
(constraint (= (f #x538b8ca09eca45d2) #x538b8ca09eca45d4))
(constraint (= (f #x25e279e3de9c9404) #x25e279e3de9c9406))
(constraint (= (f #x78d28d6626ed2c73) #xe34a35989bb4b1cc))
(constraint (= (f #x622022498b2e7580) #x622022498b2e7582))
(constraint (= (f #xae095024ed1311c7) #xb8254093b44c471c))
(constraint (= (f #x6785d795c86e775e) #x6785d795c86e7760))
(constraint (= (f #x17c63483c5848262) #x17c63483c5848264))
(constraint (= (f #x35e138b3429555da) #xd784e2cd0a555768))
(constraint (= (f #x86e50731ab17d8cd) #x1b941cc6ac5f6334))
(constraint (= (f #x6de7ceaa93abac63) #xb79f3aaa4eaeb18c))
(constraint (= (f #x9e7b139ea0bedb67) #x0000000000000002))
(constraint (= (f #x520035e2319c45d4) #x520035e2319c45d6))
(constraint (= (f #x31d99dbee584c6aa) #x31d99dbee584c6ac))
(constraint (= (f #x579ea3e2edda2d97) #x0000000000000002))
(constraint (= (f #xbe238ed4c3cee5a8) #xbe238ed4c3cee5aa))
(constraint (= (f #x0739bc9c91147030) #x0739bc9c91147032))
(constraint (= (f #xea554da3dc3d2a5e) #xa955368f70f4a978))
(constraint (= (f #xe7bebe72c8629bb9) #x0000000000000002))
(constraint (= (f #xdb8c5947ad5e555e) #xdb8c5947ad5e5560))
(constraint (= (f #xea25c8c8484a297e) #xea25c8c8484a2980))
(constraint (= (f #xac3b8a5ee7dd0922) #xb0ee297b9f742488))
(constraint (= (f #x9e832e49616054db) #x0000000000000002))
(constraint (= (f #x7c09add7e30c57e6) #x7c09add7e30c57e8))
(constraint (= (f #x59e68ea6d21dce37) #x679a3a9b487738dc))
(constraint (= (f #x35d78bdc9863eeb5) #xd75e2f72618fbad4))
(constraint (= (f #x0a6ebea02b186946) #x0a6ebea02b186948))
(constraint (= (f #x576773102b71ae60) #x5d9dcc40adc6b980))
(constraint (= (f #xdbe8710c477c10e3) #x0000000000000002))
(constraint (= (f #x57296d97ad929684) #x57296d97ad929686))
(constraint (= (f #x1678139713b57428) #x59e04e5c4ed5d0a0))
(constraint (= (f #x23852ee3d526526e) #x23852ee3d5265270))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvand #x0000000000000001 x) #x0000000000000000) (ite (= (bvsrem x #x000000000000000e) #x0000000000000000) (ite (= (bvurem x #x000000000000000c) #x0000000000000000) (bvmul #x0000000000000004 x) (ite (= (bvand #x0000000000000008 x) #x0000000000000000) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (ite (= (bvsrem x #x000000000000000a) #x0000000000000000) (bvadd #x0000000000000002 x) (bvmul #x0000000000000004 x)) (bvadd #x0000000000000002 x)) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (bvmul #x0000000000000004 x) (bvadd #x0000000000000002 x)) (bvmul #x0000000000000004 x)))) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (bvadd #x0000000000000002 x) (ite (= (bvurem x #x000000000000000c) #x0000000000000000) (bvadd #x0000000000000002 x) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (ite (= (bvurem x #x000000000000000e) #x0000000000000000) (bvmul #x0000000000000004 x) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (ite (= (bvsrem x #x000000000000000c) #x0000000000000000) (ite (= (bvsrem x #x000000000000000a) #x0000000000000000) (bvadd #x0000000000000002 x) (bvmul #x0000000000000004 x)) (bvadd #x0000000000000002 x)) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) (bvmul #x0000000000000004 x) (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (bvadd #x0000000000000002 x) (ite (= (bvor #x0000000000000006 x) x) (bvmul #x0000000000000004 x) (bvadd #x0000000000000002 x)))))) (ite (= (bvurem x #x000000000000000d) #x0000000000000000) (bvmul #x0000000000000004 x) (ite (= (bvurem x #x0000000000000005) #x0000000000000001) (ite (= (bvor #x0000000000000006 x) x) (bvmul #x0000000000000004 x) (ite (= (bvor #x000000000000000a x) x) (bvmul #x0000000000000004 x) (bvadd #x0000000000000002 x))) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) (bvmul #x0000000000000004 x) (bvadd #x0000000000000002 x)))))))) (ite (= (bvurem x #x0000000000000007) #x0000000000000001) #x0000000000000002 (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvurem x #x0000000000000009) #x0000000000000000) (ite (= (bvand #x0000000000000008 x) #x0000000000000000) #x0000000000000002 (bvmul #x0000000000000004 x)) (bvmul #x0000000000000004 x)) (ite (= (bvurem x #x0000000000000007) #x0000000000000000) (bvmul #x0000000000000004 x) (ite (= (bvsrem x #x000000000000000d) #x0000000000000000) #x0000000000000002 (ite (= (bvurem x #x000000000000000b) #x0000000000000001) (ite (= (bvurem x #x0000000000000006) #x0000000000000001) (bvmul #x0000000000000004 x) #x0000000000000002) (ite (= (bvor #x0000000000000006 x) x) #x0000000000000002 (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (bvmul #x0000000000000004 x) (ite (= (bvurem x #x000000000000000a) #x0000000000000001) #x0000000000000002 (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (bvmul #x0000000000000004 x) (ite (= (bvurem x #x000000000000000b) #x0000000000000000) (bvmul #x0000000000000004 x) #x0000000000000002))))))))))))
